(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(and(tt, z0)) → mark(z0)
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(s(plus(z0, z1)))
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
Tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c2(MARK(s(plus(z0, z1))), S(plus(z0, z1)), PLUS(z0, z1))
MARK(and(z0, z1)) → c3(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(tt) → c4(ACTIVE(tt))
MARK(plus(z0, z1)) → c5(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(0) → c6(ACTIVE(0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
S tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c2(MARK(s(plus(z0, z1))), S(plus(z0, z1)), PLUS(z0, z1))
MARK(and(z0, z1)) → c3(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(tt) → c4(ACTIVE(tt))
MARK(plus(z0, z1)) → c5(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(0) → c6(ACTIVE(0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
K tuples:none
Defined Rule Symbols:
active, mark, and, plus, s
Defined Pair Symbols:
ACTIVE, MARK, AND, PLUS, S
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
MARK(0) → c6(ACTIVE(0))
MARK(tt) → c4(ACTIVE(tt))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(and(tt, z0)) → mark(z0)
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(s(plus(z0, z1)))
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
Tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c2(MARK(s(plus(z0, z1))), S(plus(z0, z1)), PLUS(z0, z1))
MARK(and(z0, z1)) → c3(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) → c5(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
S tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
ACTIVE(plus(z0, s(z1))) → c2(MARK(s(plus(z0, z1))), S(plus(z0, z1)), PLUS(z0, z1))
MARK(and(z0, z1)) → c3(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) → c5(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
K tuples:none
Defined Rule Symbols:
active, mark, and, plus, s
Defined Pair Symbols:
ACTIVE, MARK, AND, PLUS, S
Compound Symbols:
c, c1, c2, c3, c5, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
ACTIVE(
plus(
z0,
s(
z1))) →
c2(
MARK(
s(
plus(
z0,
z1))),
S(
plus(
z0,
z1)),
PLUS(
z0,
z1)) by
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(and(tt, z0)) → mark(z0)
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(s(plus(z0, z1)))
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
Tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
MARK(and(z0, z1)) → c3(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) → c5(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
S tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
MARK(and(z0, z1)) → c3(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) → c5(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
K tuples:none
Defined Rule Symbols:
active, mark, and, plus, s
Defined Pair Symbols:
ACTIVE, MARK, AND, PLUS, S
Compound Symbols:
c, c1, c3, c5, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c2
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
MARK(
and(
z0,
z1)) →
c3(
ACTIVE(
and(
mark(
z0),
z1)),
AND(
mark(
z0),
z1),
MARK(
z0)) by
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(and(z0, z1), x1)) → c3(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(and(tt, z0)) → mark(z0)
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(s(plus(z0, z1)))
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
Tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
MARK(plus(z0, z1)) → c5(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(and(z0, z1), x1)) → c3(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
S tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
MARK(plus(z0, z1)) → c5(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(and(z0, z1), x1)) → c3(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
K tuples:none
Defined Rule Symbols:
active, mark, and, plus, s
Defined Pair Symbols:
ACTIVE, MARK, AND, PLUS, S
Compound Symbols:
c, c1, c5, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c2, c3, c3
(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
MARK(
plus(
z0,
z1)) →
c5(
ACTIVE(
plus(
mark(
z0),
mark(
z1))),
PLUS(
mark(
z0),
mark(
z1)),
MARK(
z0),
MARK(
z1)) by
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(x0, x1)) → c5
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(and(tt, z0)) → mark(z0)
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(s(plus(z0, z1)))
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
Tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(and(z0, z1), x1)) → c3(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(x0, x1)) → c5
S tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(and(z0, z1), x1)) → c3(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(plus(x0, x1)) → c5
K tuples:none
Defined Rule Symbols:
active, mark, and, plus, s
Defined Pair Symbols:
ACTIVE, MARK, AND, PLUS, S
Compound Symbols:
c, c1, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c2, c3, c3, c5, c5
(11) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
MARK(plus(x0, x1)) → c5
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(and(tt, z0)) → mark(z0)
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(s(plus(z0, z1)))
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
Tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(and(z0, z1), x1)) → c3(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
S tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
MARK(s(z0)) → c7(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(and(z0, z1), x1)) → c3(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
K tuples:none
Defined Rule Symbols:
active, mark, and, plus, s
Defined Pair Symbols:
ACTIVE, MARK, AND, PLUS, S
Compound Symbols:
c, c1, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c2, c3, c3, c5
(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
MARK(
s(
z0)) →
c7(
ACTIVE(
s(
mark(
z0))),
S(
mark(
z0)),
MARK(
z0)) by
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(and(z0, z1))) → c7(ACTIVE(s(active(and(mark(z0), z1)))), S(mark(and(z0, z1))), MARK(and(z0, z1)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(x0)) → c7
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(and(tt, z0)) → mark(z0)
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(s(plus(z0, z1)))
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
Tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(and(z0, z1), x1)) → c3(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(and(z0, z1))) → c7(ACTIVE(s(active(and(mark(z0), z1)))), S(mark(and(z0, z1))), MARK(and(z0, z1)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(x0)) → c7
S tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(and(z0, z1), x1)) → c3(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(and(z0, z1))) → c7(ACTIVE(s(active(and(mark(z0), z1)))), S(mark(and(z0, z1))), MARK(and(z0, z1)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(s(x0)) → c7
K tuples:none
Defined Rule Symbols:
active, mark, and, plus, s
Defined Pair Symbols:
ACTIVE, AND, PLUS, S, MARK
Compound Symbols:
c, c1, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c2, c3, c3, c5, c7, c7
(15) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
MARK(s(x0)) → c7
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(and(tt, z0)) → mark(z0)
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(s(plus(z0, z1)))
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
Tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(and(z0, z1), x1)) → c3(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(and(z0, z1))) → c7(ACTIVE(s(active(and(mark(z0), z1)))), S(mark(and(z0, z1))), MARK(and(z0, z1)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
S tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(and(z0, z1), x1)) → c3(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(and(z0, z1))) → c7(ACTIVE(s(active(and(mark(z0), z1)))), S(mark(and(z0, z1))), MARK(and(z0, z1)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
K tuples:none
Defined Rule Symbols:
active, mark, and, plus, s
Defined Pair Symbols:
ACTIVE, AND, PLUS, S, MARK
Compound Symbols:
c, c1, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c2, c3, c3, c5, c7
(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
MARK(
and(
and(
z0,
z1),
x1)) →
c3(
ACTIVE(
and(
active(
and(
mark(
z0),
z1)),
x1)),
AND(
mark(
and(
z0,
z1)),
x1),
MARK(
and(
z0,
z1))) by
MARK(and(and(x0, x1), z1)) → c3(ACTIVE(and(and(mark(x0), x1), z1)), AND(mark(and(x0, x1)), z1), MARK(and(x0, x1)))
MARK(and(and(z0, z1), x2)) → c3(ACTIVE(and(active(and(z0, z1)), x2)), AND(mark(and(z0, z1)), x2), MARK(and(z0, z1)))
MARK(and(and(and(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(and(mark(z0), z1)), x1)), x2)), AND(mark(and(and(z0, z1), x1)), x2), MARK(and(and(z0, z1), x1)))
MARK(and(and(tt, x1), x2)) → c3(ACTIVE(and(active(and(active(tt), x1)), x2)), AND(mark(and(tt, x1)), x2), MARK(and(tt, x1)))
MARK(and(and(plus(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(plus(mark(z0), mark(z1))), x1)), x2)), AND(mark(and(plus(z0, z1), x1)), x2), MARK(and(plus(z0, z1), x1)))
MARK(and(and(0, x1), x2)) → c3(ACTIVE(and(active(and(active(0), x1)), x2)), AND(mark(and(0, x1)), x2), MARK(and(0, x1)))
MARK(and(and(s(z0), x1), x2)) → c3(ACTIVE(and(active(and(active(s(mark(z0))), x1)), x2)), AND(mark(and(s(z0), x1)), x2), MARK(and(s(z0), x1)))
MARK(and(and(x0, x1), x2)) → c3(AND(mark(and(x0, x1)), x2))
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(and(tt, z0)) → mark(z0)
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(s(plus(z0, z1)))
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
Tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(and(z0, z1))) → c7(ACTIVE(s(active(and(mark(z0), z1)))), S(mark(and(z0, z1))), MARK(and(z0, z1)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(and(and(x0, x1), z1)) → c3(ACTIVE(and(and(mark(x0), x1), z1)), AND(mark(and(x0, x1)), z1), MARK(and(x0, x1)))
MARK(and(and(z0, z1), x2)) → c3(ACTIVE(and(active(and(z0, z1)), x2)), AND(mark(and(z0, z1)), x2), MARK(and(z0, z1)))
MARK(and(and(and(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(and(mark(z0), z1)), x1)), x2)), AND(mark(and(and(z0, z1), x1)), x2), MARK(and(and(z0, z1), x1)))
MARK(and(and(tt, x1), x2)) → c3(ACTIVE(and(active(and(active(tt), x1)), x2)), AND(mark(and(tt, x1)), x2), MARK(and(tt, x1)))
MARK(and(and(plus(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(plus(mark(z0), mark(z1))), x1)), x2)), AND(mark(and(plus(z0, z1), x1)), x2), MARK(and(plus(z0, z1), x1)))
MARK(and(and(0, x1), x2)) → c3(ACTIVE(and(active(and(active(0), x1)), x2)), AND(mark(and(0, x1)), x2), MARK(and(0, x1)))
MARK(and(and(s(z0), x1), x2)) → c3(ACTIVE(and(active(and(active(s(mark(z0))), x1)), x2)), AND(mark(and(s(z0), x1)), x2), MARK(and(s(z0), x1)))
MARK(and(and(x0, x1), x2)) → c3(AND(mark(and(x0, x1)), x2))
S tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(tt, x1)) → c3(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(and(z0, z1))) → c7(ACTIVE(s(active(and(mark(z0), z1)))), S(mark(and(z0, z1))), MARK(and(z0, z1)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(and(and(x0, x1), z1)) → c3(ACTIVE(and(and(mark(x0), x1), z1)), AND(mark(and(x0, x1)), z1), MARK(and(x0, x1)))
MARK(and(and(z0, z1), x2)) → c3(ACTIVE(and(active(and(z0, z1)), x2)), AND(mark(and(z0, z1)), x2), MARK(and(z0, z1)))
MARK(and(and(and(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(and(mark(z0), z1)), x1)), x2)), AND(mark(and(and(z0, z1), x1)), x2), MARK(and(and(z0, z1), x1)))
MARK(and(and(tt, x1), x2)) → c3(ACTIVE(and(active(and(active(tt), x1)), x2)), AND(mark(and(tt, x1)), x2), MARK(and(tt, x1)))
MARK(and(and(plus(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(plus(mark(z0), mark(z1))), x1)), x2)), AND(mark(and(plus(z0, z1), x1)), x2), MARK(and(plus(z0, z1), x1)))
MARK(and(and(0, x1), x2)) → c3(ACTIVE(and(active(and(active(0), x1)), x2)), AND(mark(and(0, x1)), x2), MARK(and(0, x1)))
MARK(and(and(s(z0), x1), x2)) → c3(ACTIVE(and(active(and(active(s(mark(z0))), x1)), x2)), AND(mark(and(s(z0), x1)), x2), MARK(and(s(z0), x1)))
MARK(and(and(x0, x1), x2)) → c3(AND(mark(and(x0, x1)), x2))
K tuples:none
Defined Rule Symbols:
active, mark, and, plus, s
Defined Pair Symbols:
ACTIVE, AND, PLUS, S, MARK
Compound Symbols:
c, c1, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c2, c3, c3, c5, c7
(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
MARK(
and(
tt,
x1)) →
c3(
ACTIVE(
and(
active(
tt),
x1)),
AND(
mark(
tt),
x1),
MARK(
tt)) by
MARK(and(tt, z1)) → c3(ACTIVE(and(tt, z1)), AND(mark(tt), z1), MARK(tt))
MARK(and(tt, x0)) → c3(AND(mark(tt), x0))
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(and(tt, z0)) → mark(z0)
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(s(plus(z0, z1)))
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
Tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(and(z0, z1))) → c7(ACTIVE(s(active(and(mark(z0), z1)))), S(mark(and(z0, z1))), MARK(and(z0, z1)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(and(and(x0, x1), z1)) → c3(ACTIVE(and(and(mark(x0), x1), z1)), AND(mark(and(x0, x1)), z1), MARK(and(x0, x1)))
MARK(and(and(z0, z1), x2)) → c3(ACTIVE(and(active(and(z0, z1)), x2)), AND(mark(and(z0, z1)), x2), MARK(and(z0, z1)))
MARK(and(and(and(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(and(mark(z0), z1)), x1)), x2)), AND(mark(and(and(z0, z1), x1)), x2), MARK(and(and(z0, z1), x1)))
MARK(and(and(tt, x1), x2)) → c3(ACTIVE(and(active(and(active(tt), x1)), x2)), AND(mark(and(tt, x1)), x2), MARK(and(tt, x1)))
MARK(and(and(plus(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(plus(mark(z0), mark(z1))), x1)), x2)), AND(mark(and(plus(z0, z1), x1)), x2), MARK(and(plus(z0, z1), x1)))
MARK(and(and(0, x1), x2)) → c3(ACTIVE(and(active(and(active(0), x1)), x2)), AND(mark(and(0, x1)), x2), MARK(and(0, x1)))
MARK(and(and(s(z0), x1), x2)) → c3(ACTIVE(and(active(and(active(s(mark(z0))), x1)), x2)), AND(mark(and(s(z0), x1)), x2), MARK(and(s(z0), x1)))
MARK(and(and(x0, x1), x2)) → c3(AND(mark(and(x0, x1)), x2))
MARK(and(tt, z1)) → c3(ACTIVE(and(tt, z1)), AND(mark(tt), z1), MARK(tt))
MARK(and(tt, x0)) → c3(AND(mark(tt), x0))
S tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(plus(z0, z1), x1)) → c3(ACTIVE(and(active(plus(mark(z0), mark(z1))), x1)), AND(mark(plus(z0, z1)), x1), MARK(plus(z0, z1)))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(and(z0, z1))) → c7(ACTIVE(s(active(and(mark(z0), z1)))), S(mark(and(z0, z1))), MARK(and(z0, z1)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(and(and(x0, x1), z1)) → c3(ACTIVE(and(and(mark(x0), x1), z1)), AND(mark(and(x0, x1)), z1), MARK(and(x0, x1)))
MARK(and(and(z0, z1), x2)) → c3(ACTIVE(and(active(and(z0, z1)), x2)), AND(mark(and(z0, z1)), x2), MARK(and(z0, z1)))
MARK(and(and(and(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(and(mark(z0), z1)), x1)), x2)), AND(mark(and(and(z0, z1), x1)), x2), MARK(and(and(z0, z1), x1)))
MARK(and(and(tt, x1), x2)) → c3(ACTIVE(and(active(and(active(tt), x1)), x2)), AND(mark(and(tt, x1)), x2), MARK(and(tt, x1)))
MARK(and(and(plus(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(plus(mark(z0), mark(z1))), x1)), x2)), AND(mark(and(plus(z0, z1), x1)), x2), MARK(and(plus(z0, z1), x1)))
MARK(and(and(0, x1), x2)) → c3(ACTIVE(and(active(and(active(0), x1)), x2)), AND(mark(and(0, x1)), x2), MARK(and(0, x1)))
MARK(and(and(s(z0), x1), x2)) → c3(ACTIVE(and(active(and(active(s(mark(z0))), x1)), x2)), AND(mark(and(s(z0), x1)), x2), MARK(and(s(z0), x1)))
MARK(and(and(x0, x1), x2)) → c3(AND(mark(and(x0, x1)), x2))
MARK(and(tt, z1)) → c3(ACTIVE(and(tt, z1)), AND(mark(tt), z1), MARK(tt))
MARK(and(tt, x0)) → c3(AND(mark(tt), x0))
K tuples:none
Defined Rule Symbols:
active, mark, and, plus, s
Defined Pair Symbols:
ACTIVE, AND, PLUS, S, MARK
Compound Symbols:
c, c1, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c2, c3, c3, c5, c7
(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
MARK(
and(
plus(
z0,
z1),
x1)) →
c3(
ACTIVE(
and(
active(
plus(
mark(
z0),
mark(
z1))),
x1)),
AND(
mark(
plus(
z0,
z1)),
x1),
MARK(
plus(
z0,
z1))) by
MARK(and(plus(x0, x1), z1)) → c3(ACTIVE(and(plus(mark(x0), mark(x1)), z1)), AND(mark(plus(x0, x1)), z1), MARK(plus(x0, x1)))
MARK(and(plus(z0, x1), x2)) → c3(ACTIVE(and(active(plus(z0, mark(x1))), x2)), AND(mark(plus(z0, x1)), x2), MARK(plus(z0, x1)))
MARK(and(plus(x0, z1), x2)) → c3(ACTIVE(and(active(plus(mark(x0), z1)), x2)), AND(mark(plus(x0, z1)), x2), MARK(plus(x0, z1)))
MARK(and(plus(x0, and(z0, z1)), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(and(mark(z0), z1)))), x2)), AND(mark(plus(x0, and(z0, z1))), x2), MARK(plus(x0, and(z0, z1))))
MARK(and(plus(x0, tt), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(tt))), x2)), AND(mark(plus(x0, tt)), x2), MARK(plus(x0, tt)))
MARK(and(plus(x0, plus(z0, z1)), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(plus(mark(z0), mark(z1))))), x2)), AND(mark(plus(x0, plus(z0, z1))), x2), MARK(plus(x0, plus(z0, z1))))
MARK(and(plus(x0, 0), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(0))), x2)), AND(mark(plus(x0, 0)), x2), MARK(plus(x0, 0)))
MARK(and(plus(x0, s(z0)), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(s(mark(z0))))), x2)), AND(mark(plus(x0, s(z0))), x2), MARK(plus(x0, s(z0))))
MARK(and(plus(and(z0, z1), x1), x2)) → c3(ACTIVE(and(active(plus(active(and(mark(z0), z1)), mark(x1))), x2)), AND(mark(plus(and(z0, z1), x1)), x2), MARK(plus(and(z0, z1), x1)))
MARK(and(plus(tt, x1), x2)) → c3(ACTIVE(and(active(plus(active(tt), mark(x1))), x2)), AND(mark(plus(tt, x1)), x2), MARK(plus(tt, x1)))
MARK(and(plus(plus(z0, z1), x1), x2)) → c3(ACTIVE(and(active(plus(active(plus(mark(z0), mark(z1))), mark(x1))), x2)), AND(mark(plus(plus(z0, z1), x1)), x2), MARK(plus(plus(z0, z1), x1)))
MARK(and(plus(0, x1), x2)) → c3(ACTIVE(and(active(plus(active(0), mark(x1))), x2)), AND(mark(plus(0, x1)), x2), MARK(plus(0, x1)))
MARK(and(plus(s(z0), x1), x2)) → c3(ACTIVE(and(active(plus(active(s(mark(z0))), mark(x1))), x2)), AND(mark(plus(s(z0), x1)), x2), MARK(plus(s(z0), x1)))
MARK(and(plus(x0, x1), x2)) → c3(AND(mark(plus(x0, x1)), x2), MARK(plus(x0, x1)))
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(and(tt, z0)) → mark(z0)
active(plus(z0, 0)) → mark(z0)
active(plus(z0, s(z1))) → mark(s(plus(z0, z1)))
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
Tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(and(z0, z1))) → c7(ACTIVE(s(active(and(mark(z0), z1)))), S(mark(and(z0, z1))), MARK(and(z0, z1)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(and(and(x0, x1), z1)) → c3(ACTIVE(and(and(mark(x0), x1), z1)), AND(mark(and(x0, x1)), z1), MARK(and(x0, x1)))
MARK(and(and(z0, z1), x2)) → c3(ACTIVE(and(active(and(z0, z1)), x2)), AND(mark(and(z0, z1)), x2), MARK(and(z0, z1)))
MARK(and(and(and(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(and(mark(z0), z1)), x1)), x2)), AND(mark(and(and(z0, z1), x1)), x2), MARK(and(and(z0, z1), x1)))
MARK(and(and(tt, x1), x2)) → c3(ACTIVE(and(active(and(active(tt), x1)), x2)), AND(mark(and(tt, x1)), x2), MARK(and(tt, x1)))
MARK(and(and(plus(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(plus(mark(z0), mark(z1))), x1)), x2)), AND(mark(and(plus(z0, z1), x1)), x2), MARK(and(plus(z0, z1), x1)))
MARK(and(and(0, x1), x2)) → c3(ACTIVE(and(active(and(active(0), x1)), x2)), AND(mark(and(0, x1)), x2), MARK(and(0, x1)))
MARK(and(and(s(z0), x1), x2)) → c3(ACTIVE(and(active(and(active(s(mark(z0))), x1)), x2)), AND(mark(and(s(z0), x1)), x2), MARK(and(s(z0), x1)))
MARK(and(and(x0, x1), x2)) → c3(AND(mark(and(x0, x1)), x2))
MARK(and(tt, z1)) → c3(ACTIVE(and(tt, z1)), AND(mark(tt), z1), MARK(tt))
MARK(and(tt, x0)) → c3(AND(mark(tt), x0))
MARK(and(plus(x0, x1), z1)) → c3(ACTIVE(and(plus(mark(x0), mark(x1)), z1)), AND(mark(plus(x0, x1)), z1), MARK(plus(x0, x1)))
MARK(and(plus(z0, x1), x2)) → c3(ACTIVE(and(active(plus(z0, mark(x1))), x2)), AND(mark(plus(z0, x1)), x2), MARK(plus(z0, x1)))
MARK(and(plus(x0, z1), x2)) → c3(ACTIVE(and(active(plus(mark(x0), z1)), x2)), AND(mark(plus(x0, z1)), x2), MARK(plus(x0, z1)))
MARK(and(plus(x0, and(z0, z1)), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(and(mark(z0), z1)))), x2)), AND(mark(plus(x0, and(z0, z1))), x2), MARK(plus(x0, and(z0, z1))))
MARK(and(plus(x0, tt), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(tt))), x2)), AND(mark(plus(x0, tt)), x2), MARK(plus(x0, tt)))
MARK(and(plus(x0, plus(z0, z1)), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(plus(mark(z0), mark(z1))))), x2)), AND(mark(plus(x0, plus(z0, z1))), x2), MARK(plus(x0, plus(z0, z1))))
MARK(and(plus(x0, 0), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(0))), x2)), AND(mark(plus(x0, 0)), x2), MARK(plus(x0, 0)))
MARK(and(plus(x0, s(z0)), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(s(mark(z0))))), x2)), AND(mark(plus(x0, s(z0))), x2), MARK(plus(x0, s(z0))))
MARK(and(plus(and(z0, z1), x1), x2)) → c3(ACTIVE(and(active(plus(active(and(mark(z0), z1)), mark(x1))), x2)), AND(mark(plus(and(z0, z1), x1)), x2), MARK(plus(and(z0, z1), x1)))
MARK(and(plus(tt, x1), x2)) → c3(ACTIVE(and(active(plus(active(tt), mark(x1))), x2)), AND(mark(plus(tt, x1)), x2), MARK(plus(tt, x1)))
MARK(and(plus(plus(z0, z1), x1), x2)) → c3(ACTIVE(and(active(plus(active(plus(mark(z0), mark(z1))), mark(x1))), x2)), AND(mark(plus(plus(z0, z1), x1)), x2), MARK(plus(plus(z0, z1), x1)))
MARK(and(plus(0, x1), x2)) → c3(ACTIVE(and(active(plus(active(0), mark(x1))), x2)), AND(mark(plus(0, x1)), x2), MARK(plus(0, x1)))
MARK(and(plus(s(z0), x1), x2)) → c3(ACTIVE(and(active(plus(active(s(mark(z0))), mark(x1))), x2)), AND(mark(plus(s(z0), x1)), x2), MARK(plus(s(z0), x1)))
MARK(and(plus(x0, x1), x2)) → c3(AND(mark(plus(x0, x1)), x2), MARK(plus(x0, x1)))
S tuples:
ACTIVE(and(tt, z0)) → c(MARK(z0))
ACTIVE(plus(z0, 0)) → c1(MARK(z0))
AND(mark(z0), z1) → c8(AND(z0, z1))
AND(z0, mark(z1)) → c9(AND(z0, z1))
AND(active(z0), z1) → c10(AND(z0, z1))
AND(z0, active(z1)) → c11(AND(z0, z1))
PLUS(mark(z0), z1) → c12(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c13(PLUS(z0, z1))
PLUS(active(z0), z1) → c14(PLUS(z0, z1))
PLUS(z0, active(z1)) → c15(PLUS(z0, z1))
S(mark(z0)) → c16(S(z0))
S(active(z0)) → c17(S(z0))
ACTIVE(plus(x0, s(x1))) → c2(MARK(s(plus(x0, x1))), PLUS(x0, x1))
MARK(and(z0, z1)) → c3(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(0, x1)) → c3(ACTIVE(and(active(0), x1)), AND(mark(0), x1), MARK(0))
MARK(and(s(z0), x1)) → c3(ACTIVE(and(active(s(mark(z0))), x1)), AND(mark(s(z0)), x1), MARK(s(z0)))
MARK(and(x0, x1)) → c3(AND(mark(x0), x1))
MARK(plus(z0, x1)) → c5(ACTIVE(plus(z0, mark(x1))), PLUS(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(plus(x0, z1)) → c5(ACTIVE(plus(mark(x0), z1)), PLUS(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(plus(x0, and(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(and(mark(z0), z1)))), PLUS(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(plus(x0, tt)) → c5(ACTIVE(plus(mark(x0), active(tt))), PLUS(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(plus(x0, plus(z0, z1))) → c5(ACTIVE(plus(mark(x0), active(plus(mark(z0), mark(z1))))), PLUS(mark(x0), mark(plus(z0, z1))), MARK(x0), MARK(plus(z0, z1)))
MARK(plus(x0, 0)) → c5(ACTIVE(plus(mark(x0), active(0))), PLUS(mark(x0), mark(0)), MARK(x0), MARK(0))
MARK(plus(x0, s(z0))) → c5(ACTIVE(plus(mark(x0), active(s(mark(z0))))), PLUS(mark(x0), mark(s(z0))), MARK(x0), MARK(s(z0)))
MARK(plus(and(z0, z1), x1)) → c5(ACTIVE(plus(active(and(mark(z0), z1)), mark(x1))), PLUS(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(plus(tt, x1)) → c5(ACTIVE(plus(active(tt), mark(x1))), PLUS(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(plus(plus(z0, z1), x1)) → c5(ACTIVE(plus(active(plus(mark(z0), mark(z1))), mark(x1))), PLUS(mark(plus(z0, z1)), mark(x1)), MARK(plus(z0, z1)), MARK(x1))
MARK(plus(0, x1)) → c5(ACTIVE(plus(active(0), mark(x1))), PLUS(mark(0), mark(x1)), MARK(0), MARK(x1))
MARK(plus(s(z0), x1)) → c5(ACTIVE(plus(active(s(mark(z0))), mark(x1))), PLUS(mark(s(z0)), mark(x1)), MARK(s(z0)), MARK(x1))
MARK(s(z0)) → c7(ACTIVE(s(z0)), S(mark(z0)), MARK(z0))
MARK(s(and(z0, z1))) → c7(ACTIVE(s(active(and(mark(z0), z1)))), S(mark(and(z0, z1))), MARK(and(z0, z1)))
MARK(s(tt)) → c7(ACTIVE(s(active(tt))), S(mark(tt)), MARK(tt))
MARK(s(plus(z0, z1))) → c7(ACTIVE(s(active(plus(mark(z0), mark(z1))))), S(mark(plus(z0, z1))), MARK(plus(z0, z1)))
MARK(s(0)) → c7(ACTIVE(s(active(0))), S(mark(0)), MARK(0))
MARK(s(s(z0))) → c7(ACTIVE(s(active(s(mark(z0))))), S(mark(s(z0))), MARK(s(z0)))
MARK(and(and(x0, x1), z1)) → c3(ACTIVE(and(and(mark(x0), x1), z1)), AND(mark(and(x0, x1)), z1), MARK(and(x0, x1)))
MARK(and(and(z0, z1), x2)) → c3(ACTIVE(and(active(and(z0, z1)), x2)), AND(mark(and(z0, z1)), x2), MARK(and(z0, z1)))
MARK(and(and(and(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(and(mark(z0), z1)), x1)), x2)), AND(mark(and(and(z0, z1), x1)), x2), MARK(and(and(z0, z1), x1)))
MARK(and(and(tt, x1), x2)) → c3(ACTIVE(and(active(and(active(tt), x1)), x2)), AND(mark(and(tt, x1)), x2), MARK(and(tt, x1)))
MARK(and(and(plus(z0, z1), x1), x2)) → c3(ACTIVE(and(active(and(active(plus(mark(z0), mark(z1))), x1)), x2)), AND(mark(and(plus(z0, z1), x1)), x2), MARK(and(plus(z0, z1), x1)))
MARK(and(and(0, x1), x2)) → c3(ACTIVE(and(active(and(active(0), x1)), x2)), AND(mark(and(0, x1)), x2), MARK(and(0, x1)))
MARK(and(and(s(z0), x1), x2)) → c3(ACTIVE(and(active(and(active(s(mark(z0))), x1)), x2)), AND(mark(and(s(z0), x1)), x2), MARK(and(s(z0), x1)))
MARK(and(and(x0, x1), x2)) → c3(AND(mark(and(x0, x1)), x2))
MARK(and(tt, z1)) → c3(ACTIVE(and(tt, z1)), AND(mark(tt), z1), MARK(tt))
MARK(and(tt, x0)) → c3(AND(mark(tt), x0))
MARK(and(plus(x0, x1), z1)) → c3(ACTIVE(and(plus(mark(x0), mark(x1)), z1)), AND(mark(plus(x0, x1)), z1), MARK(plus(x0, x1)))
MARK(and(plus(z0, x1), x2)) → c3(ACTIVE(and(active(plus(z0, mark(x1))), x2)), AND(mark(plus(z0, x1)), x2), MARK(plus(z0, x1)))
MARK(and(plus(x0, z1), x2)) → c3(ACTIVE(and(active(plus(mark(x0), z1)), x2)), AND(mark(plus(x0, z1)), x2), MARK(plus(x0, z1)))
MARK(and(plus(x0, and(z0, z1)), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(and(mark(z0), z1)))), x2)), AND(mark(plus(x0, and(z0, z1))), x2), MARK(plus(x0, and(z0, z1))))
MARK(and(plus(x0, tt), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(tt))), x2)), AND(mark(plus(x0, tt)), x2), MARK(plus(x0, tt)))
MARK(and(plus(x0, plus(z0, z1)), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(plus(mark(z0), mark(z1))))), x2)), AND(mark(plus(x0, plus(z0, z1))), x2), MARK(plus(x0, plus(z0, z1))))
MARK(and(plus(x0, 0), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(0))), x2)), AND(mark(plus(x0, 0)), x2), MARK(plus(x0, 0)))
MARK(and(plus(x0, s(z0)), x2)) → c3(ACTIVE(and(active(plus(mark(x0), active(s(mark(z0))))), x2)), AND(mark(plus(x0, s(z0))), x2), MARK(plus(x0, s(z0))))
MARK(and(plus(and(z0, z1), x1), x2)) → c3(ACTIVE(and(active(plus(active(and(mark(z0), z1)), mark(x1))), x2)), AND(mark(plus(and(z0, z1), x1)), x2), MARK(plus(and(z0, z1), x1)))
MARK(and(plus(tt, x1), x2)) → c3(ACTIVE(and(active(plus(active(tt), mark(x1))), x2)), AND(mark(plus(tt, x1)), x2), MARK(plus(tt, x1)))
MARK(and(plus(plus(z0, z1), x1), x2)) → c3(ACTIVE(and(active(plus(active(plus(mark(z0), mark(z1))), mark(x1))), x2)), AND(mark(plus(plus(z0, z1), x1)), x2), MARK(plus(plus(z0, z1), x1)))
MARK(and(plus(0, x1), x2)) → c3(ACTIVE(and(active(plus(active(0), mark(x1))), x2)), AND(mark(plus(0, x1)), x2), MARK(plus(0, x1)))
MARK(and(plus(s(z0), x1), x2)) → c3(ACTIVE(and(active(plus(active(s(mark(z0))), mark(x1))), x2)), AND(mark(plus(s(z0), x1)), x2), MARK(plus(s(z0), x1)))
MARK(and(plus(x0, x1), x2)) → c3(AND(mark(plus(x0, x1)), x2), MARK(plus(x0, x1)))
K tuples:none
Defined Rule Symbols:
active, mark, and, plus, s
Defined Pair Symbols:
ACTIVE, AND, PLUS, S, MARK
Compound Symbols:
c, c1, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c2, c3, c3, c5, c7, c3
(23) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5]
transitions:
tt0() → 0
00() → 0
active0(0) → 1
mark0(0) → 2
and0(0, 0) → 3
plus0(0, 0) → 4
s0(0) → 5
tt1() → 6
active1(6) → 2
01() → 7
active1(7) → 2
(24) BOUNDS(O(1), O(n^1))